(declare-fun var0 () (_ BitVec 1))
(assert (or (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (or (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (and (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1)))) (not (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1)))) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (not (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1)))) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1))) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1)))))
(assert (and (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge (bvsub var0 (bvxnor var0 var0)) (_ bv1 1)) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1))) (bvuge var0 (bvsub (bvxnor var0) (_ bv1 1)))))
(check-sat)
